Examples and exercises about formalization mathematics in Lean

Abstract: I will give several examples of formalization of small results in Lean, both starting from scratch and using Mathlib. The goal of this final day is to let the audience ''play'' with Lean in practice, proving real world theorems.

Mathematics

Audience: undergraduates

An introduction to proof assistants: a mini course about mathematical formalization

Series comments: The goal of this mini-course is to give an introduction to formalization of mathematics. I will explain what formalizing mathematics means and why it is interesting and useful for people interested in "standard" mathematics. I will show how this is done in practice using Lean, one of the several proof assistants available today. This is not a course in logic nor foundations of mathematics, in particular no prior knowledge of these topics is needed.